Inference at * 2 
Iof proof for Lemma eqtt to assert:



1. b : 
2. b
  b = tt 

latex

 by BoolInd 1 

latex

 1: 

 1: 1. tt
 1:   tt = tt
 2: 

 2: 1. ff
 2:   ff = tt
 .

Definitions

t  T, Unit, , ff, , tt